Inference at * 1 1 
Iof proof for Lemma p-fun-exp-add1-sq:



1. A : Type
2. f : A(A + Top)
3. x : A
4. isl(f(x))
  (f o p-id()  (x)) ~ (p-id()(outl(f(x)))) 

latex

 by RepUR ``p-id p-compose do-apply can-apply`` ( 0) 

latex

 1: 

 1:   (f(x)) ~ (inl outl(f(x)) )
 .

Definitions

f o g  , p-id(), can-apply(f;x), do-apply(f;x)